PolCert/syntax/SPolIRs.v at main · verif-scop/PolCert · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
Require Import PolIRs.
Require Import SInstr.
Require Import PolyLang.
Require Import PolyLoop.
Require Import Loop.
Require Import Result.
Require Import OpenScop.
Require Import String.

Local Open Scope string_scope.

Module SPolIRs <: POLIRS with Module Instr := SInstr.
  Module Instr := SInstr.
  Module State := State.
  Module Ty := Ty.
  Module PolyLang := PolyLang SInstr.
  Module PolyLoop := PolyLoop SInstr.
  Module Loop := Loop SInstr.
  Parameter scop_scheduler : OpenScop -> result OpenScop.

  Definition add_var_nodup (vars : list (Instr.ident * Ty.t)) (v : Instr.ident * Ty.t)
    : list (Instr.ident * Ty.t) :=
    if List.existsb (fun '(id, _) => Instr.ident_eqb id (fst v)) vars
    then vars
    else vars ++ (v :: nil).

  Definition export_pi_for_openscop (varctxt : list Instr.ident) (pi : PolyLang.PolyInstr)
    : PolyLang.PolyInstr :=
    let names :=
      List.app (List.map Instr.ident_to_varname varctxt)
        (List.map Instr.iterator_to_varname (List.seq 0 (PolyLang.pi_depth pi))) in
    {|
      PolyLang.pi_depth := PolyLang.pi_depth pi;
      PolyLang.pi_instr := PolyLang.pi_instr pi;
      PolyLang.pi_poly := PolyLang.pi_poly pi;
      PolyLang.pi_schedule := PolyLang.pi_schedule pi;
      PolyLang.pi_transformation := PolyLang.pi_transformation pi;
      PolyLang.pi_waccess := PolyLang.pi_waccess pi;
      PolyLang.pi_raccess :=
        PolyLang.pi_raccess pi ++ Instr.export_scalar_reads names (PolyLang.pi_instr pi);
    |}.

  Definition export_pprog_for_openscop (pol : PolyLang.t) : PolyLang.t :=
    let '(pis, varctxt, vars) := pol in
    let names :=
      List.map Instr.ident_to_varname varctxt in
    let vars' :=
      List.fold_left
        (fun acc pi =>
           List.fold_left add_var_nodup
             (Instr.export_scalar_read_vars
                (List.app names
                   (List.map Instr.iterator_to_varname (List.seq 0 (PolyLang.pi_depth pi))))
                (PolyLang.pi_instr pi))
             acc)
        pis vars in
    (List.map (export_pi_for_openscop varctxt) pis, varctxt, vars').

  Definition to_openscop_source (pol : PolyLang.t) : option OpenScop :=
    PolyLang.to_openscop (export_pprog_for_openscop pol).

  Definition scheduler cpol :=
    match to_openscop_source cpol with
    | Some inscop =>
        match scop_scheduler inscop with
      | Okk outscop =>
          match PolyLang.from_openscop_schedule_only cpol outscop with
          | Okk pol => Okk pol
          | Err msg => Err msg
          end
        | Err msg => Err msg
        end
    | None => Err "Transform pol to openscop failed"
    end.
End SPolIRs.