Merge pull request thibautbenjamin#78 from thibautbenjamin/bugfix/opp…

…osites-suspension

disambiguate opposites of suspensions

lib/translate_raw.ml

@@ -4,6 +4,13 @@ open Raw_types
 
 exception WrongNumberOfArguments
 
+let rec head_susp = function
+  | VarR _ -> 0
+  | Sub (_, _, None, _) -> 0
+  | Sub (_, _, Some susp, _) -> susp
+  | Op (_, t) | Inverse t | Unit t -> head_susp t
+  | Meta | BuiltinR _ | Letin_tm _ -> Error.fatal "ill-formed term"
+
 (* inductive translation on terms and types without let_in *)
 let rec tm t =
   let make_coh coh s susp expl =
@@ -32,8 +39,9 @@ let rec tm t =
       in
       make_coh builtin_coh s susp expl
   | Op (l, t) ->
+      let offset = head_susp t in
       let t, meta = tm t in
-      (Opposite.tm t l, meta)
+      (Opposite.tm t (List.map (fun x -> x + offset) l), meta)
   | Inverse t ->
       let t, meta_ctx = tm t in
       (Inverse.compute_inverse t, meta_ctx)

test.t/features/opposites.catt

@@ -45,3 +45,10 @@ let nested12  (x : *) (y : *) (z : *) (f : x -> y) (f' : x -> y) (f'' : x -> y)
                                     (g : y -> z) (g' : y -> z) (g'' : y -> z)
                                     (c : g -> g') (d : g' -> g'')
                                     = op { 1 2 } (comp [comp d c] [comp b a])
+
+##test interaction of opposites and suspension
+coh assoc (x(f)y(g)z(h)w) : comp f (comp g h) -> comp (comp f g) h
+coh assoc_susp (p(x(f)y(g)z(h)w)q) : comp f (comp g h) -> comp (comp f g) h
+let test (p(x(f)y(g)z(h)w)q)
+    : (op { 2 } (assoc f g h)) -> (op { 2 } (assoc f g h))
+    = id (op { 3 } (assoc_susp f g h))

test.t/run.t

@@ -187,6 +187,12 @@
   [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2 x y f f' a f'' b) z g g'' (!1builtin_comp2 y z g g' c g'' d)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
   [=^.^=] let nested12 = op_{1,2}((_builtin_comp  [(_builtin_comp  d c)] [(_builtin_comp  b a)]))
   [=I.I=] successfully defined term (builtin_comp2_func[1 1]_op{1} x y f f'' (!1builtin_comp2 x y f f' a f'' b) z g g'' (!1builtin_comp2 y z g g' c g'' d)) of type (builtin_comp2_op{1} x y f z g) -> (builtin_comp2_op{1} x y f'' z g'').
+  [=^.^=] coh assoc = (_builtin_comp  f (_builtin_comp  g h)) -> (_builtin_comp  (_builtin_comp  f g) h)
+  [=I.I=] successfully defined assoc.
+  [=^.^=] coh assoc_susp = (_builtin_comp  f (_builtin_comp  g h)) -> (_builtin_comp  (_builtin_comp  f g) h)
+  [=I.I=] successfully defined assoc_susp.
+  [=^.^=] let test = (_builtin_id  op_{3}((assoc_susp  f g h)))
+  [=I.I=] successfully defined term (!3builtin_id p q x w (!1builtin_comp2 p q x z (!1builtin_comp2 p q x y f z g) w h) (!1builtin_comp2 p q x y f w (!1builtin_comp2 p q y z g w h)) (assoc_susp_op{3} p q x y f z g w h)) of type (assoc_susp_op{3} p q x y f z g w h) -> (assoc_susp_op{3} p q x y f z g w h).
 
   $ catt features/inverses.catt
   [=^.^=] let id_inv = I((_builtin_id  x))