let sum_arities p =
let rec aux = function
- | `N _ -> 0
+ | `N _ | `Bottom | `Pacman -> 0
| `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
| `Lam(_,t) -> aux t
- | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
- | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args
+ | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many (args :> nf list)
and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
aux_many (all_terms p :> nf list)
;;
-let count_fakevars p =
- let rec aux = function
- | `N _ -> 0
- | `Var(_,ar) -> if ar = min_int then 1 else 0
- | `Lam(_,t) -> aux t
- | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
- | `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
- and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
- aux_many (all_terms p :> nf list)
-;;
-
-(* let problem_measure p = count_fakevars p, sum_arities p;;
-let string_of_measure (a,b) = "(fakevars="^string_of_int a^",sum_arities="^string_of_int b^")" *)
-
let problem_measure p = sum_arities p;;
let string_of_measure = string_of_int;;
-let print_problem label ({freshno; div; conv; ps; deltas} as p) =
+let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
Console.print_hline ();
prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||");
- let nl = "\n| " in
+ let nl = "\n " in
let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno
- ^ nl ^ "\b> DISCRIMINATING SETS (deltas)"
- ^ nl ^ deltas ^ (if deltas = "" then "" else nl)
- ^ "\b> DIVERGENT" ^ nl
- ^ "*: " ^ (match div with None -> "*" | Some div -> print ~l (div :> nf)) ^ "\n| "
- ^ "\b> CONVERGENT" ^ nl
- ^ String.concat "\n| " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else print ~l (t :> nf))) conv) ^
- (if conv = [] then "" else "\n| ")
+ ^nl^"\b> DISCRIMINATING SETS (deltas)"
+ ^nl^deltas^(if deltas = "" then "" else nl)
+ ^"\b (* DIVERGENT *)" ^ nl
+ ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\" ") ^ nl
+ ^"\b (* CONVERGENT *) [" ^ nl
+ ^ String.concat " " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
+ (if conv = [] then "" else nl)
^ "\b> NUMERIC" ^ nl
^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps)
^ nl
let failwithProblem p reason =
- print_endline (print_problem "FAIL" p);
+ print_endline (string_of_problem "FAIL" p);
failwith reason
;;
;;
let simple_expand_match ps =
- let rec aux level = function
+ let rec aux_nob level = function
| #i_num_var as t -> aux_i_num_var level t
| `Lam(b,t) -> `Lam(b,aux (level+1) t)
+ | `Pacman as t -> t
+ and aux level = function
+ | `Bottom as t -> t
+ | #nf_nob as t -> aux_nob level t
and aux_i_num_var level = function
| `Match(u,v,bs_lift,bs,args) as torig ->
let u = aux_i_num_var level u in
(match u with
| #i_n_var as u ->
let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *)
- in let t = mk_match (`N i) v bs_lift bs args in
+ in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in
if t <> torig then
aux level (t :> nf)
else raise Not_found
| _ -> raise Not_found)
with Not_found ->
- `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args))
- | `I(v,args) -> `I(v,Listx.map (aux level) args)
+ mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args))
+ | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args))
| `N _ | `Var _ as t -> t
in aux_i_num_var 0
;;
List.hd divs) div in
{p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv}
-exception ExpandedToLambda;;
-
let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) =
let len_ps = List.length ps in
(*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
| [] -> acc
| t::todo_conv ->
(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
- (* try *)
let t = subst false false x inst (t :> nf) in
(*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
let freshno,new_t,acc_new_ps =
expand_match (freshno,ps,acc_new_ps) t
in
aux' ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
- (* with ExpandedToLambda -> aux' ps (freshno,acc_conv@[`N(-1)],acc_new_ps) todo_conv *)
(* cut&paste from aux' above *)
and aux'' ps (freshno,acc_new_ps) =
bs := !bs @ [i, v] ;
freshno in
(*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*)
- let t = mk_match (`N i) orig bs_lift bs args in
+ let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
(*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
expand_match (freshno,acc_ps,acc_new_ps) t
- | `Lam _ -> raise ExpandedToLambda
+ | `Lam _ | `Pacman -> assert false (* loose typing *)
+ | `Bottom -> assert false (* algorithm invariant *)
| #i_n_var as x ->
let x = simple_expand_match (acc_ps@acc_new_ps) x in
freshno,cast_to_i_num_var x,acc_new_ps in
);
let p = {p with sigma = sigma@[x,inst]} in
let p = super_simplify p in
- prerr_endline (print_problem "instantiate" p);
+ prerr_endline (string_of_problem "instantiate" p);
p
;;
function
`N _
| `Var _
- | `Lam _ -> ()
+ | `Lam _
+ | `Pacman -> ()
| `Match(t,_,liftno,bs,args) ->
(* CSC: XXX partial dependency on the encoding *)
(match t with
function
`N _
| `Var _
- | `Lam _ -> []
+ | `Lam _
+ | `Pacman -> []
| `Match(t,_,liftno,bs,args) ->
(* CSC: XXX partial dependency on the encoding *)
(match t with
and dangerous_inert_conv arities showstoppers k args match_args more_args =
let all_args = args @ match_args in
let dangerous_args = concat_map (dangerous_conv arities showstoppers) all_args in
+ let all_args = (all_args :> nf list) in
if dangerous_args = [] then (
if List.mem k showstoppers then k :: concat_map free_vars all_args else
try
None -> aux showstoppers xs
| Some h ->
try
- dangerous arities showstoppers (x : i_n_var :> nf) ;
+ dangerous arities showstoppers (x : i_n_var :> nf_nob) ;
aux showstoppers xs
with
Dangerous ->
in
let showstoppers = sort_uniq (aux showstoppers ps) in
let dangerous_conv =
- List.map (dangerous_conv arities showstoppers) (conv :> nf list) in
+ List.map (dangerous_conv arities showstoppers) conv in
prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv;
let heads = List.sort compare (filter_map hd_of ps) in
let arities = precompute_edible_data p (uniq heads) in
let showstoppers, showstoppers_conv =
- edible arities p.div ps p.conv showstoppers in
+ edible arities p.div ps (p.conv :> nf_nob list) showstoppers in
let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
let p =
List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else
let old_conv = p.conv in
let p = { p with ps; conv } in
if l <> [] || old_conv <> conv
- then prerr_endline (print_problem "eat" p);
+ then prerr_endline (string_of_problem "eat" p);
if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then
`Finished p
else
let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in
let arities = Array.to_list (Array.make (n+1) min_int) in
let p,vars = make_fresh_vars p arities in
- let args = Listx.from_list (vars :> nf list) in
+ (* manual lifting of vars by perm in next line *)
+ let vars = List.map (function `Var (n,ar) -> `Var (n+perm,ar)) vars in
+ let args = Listx.from_list vars in
let bs = ref [] in
(* other_vars are the variables which are delayed and re-applied to the match *)
let other_vars = Array.mapi (fun n () -> `Var(n+1,min_int)) (Array.make (perm-1) ()) in
let other_vars = Array.to_list other_vars in
(* 666, since it will be replaced anyway during subst: *)
- let inst = `Match(`I((0,min_int),Listx.map (lift perm) args),(x,-666),perm,bs,other_vars) in
+ let inst = `Match(`I((0,min_int),args),(x,-666),perm,bs,other_vars) in
(* Add a number of 'perm' leading lambdas *)
let inst = Array.fold_left (fun t () -> `Lam(false, t)) inst (Array.make perm ()) in
let p = {p with deltas=bs::p.deltas} in
let compute_special_k tms =
let rec aux k (t: nf) = Pervasives.max k (match t with
| `Lam(b,t) -> aux (k + if b then 1 else 0) t
- | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
+ | `I(n, tms) -> Listx.max (Listx.map (aux 0) (tms :> nf Listx.listx))
| `Match(t, _, liftno, bs, args) ->
- List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
+ List.fold_left max 0 (List.map (aux 0) ((t :> nf)::(args :> nf list)@List.map snd !bs))
| `N _
+ | `Bottom
+ | `Pacman
| `Var _ -> 0
) in Listx.max (Listx.map (aux 0) tms)
;;
let replace_in_sigma perm =
let rec aux = function
| `N n -> `N (List.nth perm n)
+ | `Pacman
| `I _ -> assert false
| `Var _ as t -> t
| `Lam(v,t) -> `Lam(v, aux t)
| `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
+ | `Bottom as t -> t
in List.map (fun (n,t) -> (n,aux t))
in
let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in
if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then begin
p
end else
- let _ = prerr_endline (print_problem "main" p) in
+ let _ = prerr_endline (string_of_problem "main" p) in
let x,l =
match l with
| cmd::l -> cmd,l
let p_finale = aux p n cmds in
let freshno,sigma = p_finale.freshno, p_finale.sigma in
prerr_endline ("------- <DONE> ------\n ");
- (* prerr_endline (print_problem "Original problem" p); *)
+ (* prerr_endline (string_of_problem "Original problem" p); *)
prerr_endline "---------------------";
let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
prerr_endline (" BOMB == " ^ print ~l !bomb);
(* In this non-recursive version, the intermediate states may containt Matchs *)
List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps)
(p.ps :> i_num_var list) sigma in
- prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
+ prerr_endline (string_of_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ;
*)
prerr_endline "---------<OPT>----------";
let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
prerr_endline "---------<PURE>---------";
- let div = option_map (fun div -> ToScott.t_of_nf (div :> nf)) p.div in
- let conv = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.conv in
- let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in
- let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
+ let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in
+ let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in
+ let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in
+ let sigma = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in
(*let ps_ok = List.fold_left (fun ps (x,inst) ->
List.map (Pure.subst false x inst) ps) ps sigma in*)
let e = env_of_sigma freshno sigma true in
let t = Pure.mwhd (e',div,[]) in
prerr_endline ("*:: " ^ (Pure.print t));
prerr_endline (print !bomb);
- assert (t = ToScott.t_of_nf (!bomb:>nf))
+ assert (t = ToScott.scott_of_nf (!bomb:>nf))
| None -> ()) div;
List.iter (fun n ->
prerr_endline ("_::: " ^ (Pure.print n));
| I of int * nf listx
;;*)
type var = int * (* arity of variable*) int;;
-type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
-type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
-type 'nf i_num_var_ = [
- | 'nf i_n_var_
- | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
+type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ]
+type 'nf_nob i_n_var_ = [ `N of int | 'nf_nob i_var_ ]
+type ('nf_nob,'nf) i_num_var_ = [
+ | 'nf_nob i_n_var_
+ | `Match of ('nf_nob,'nf) i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf_nob list
]
-type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ]
-type nf = nf nf_
-type i_var = nf i_var_;;
-type i_n_var = nf i_n_var_;;
-type i_num_var = nf i_num_var_;;
+type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_,'nf) i_num_var_ ]
+type nf = [ nf nf_nob_ | `Bottom ]
+type nf_nob = nf nf_nob_
+type i_var = nf_nob i_var_;;
+type i_n_var = nf_nob i_n_var_;;
+type i_num_var = (nf_nob,nf) i_num_var_;;
let hd_of_i_var =
function
let aux_var l (n, ar) = (if n < l then n else n+m), ar in
let rec aux_i_num_var l =
function
- `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args)
+ `I(v,args) -> `I(aux_var l v, Listx.map (aux_nob l) args)
| `Var v -> `Var(aux_var l v)
| `N _ as x -> x
| `Match(t,v,lift,bs,args) ->
- `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args)
- and aux l =
+ `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux_nob l) args)
+ and aux_nob l =
function
- #i_num_var as x -> (aux_i_num_var l x :> nf)
+ #i_num_var as x -> (aux_i_num_var l x :> nf_nob)
| `Lam(b,nf) -> `Lam (b, aux (l+1) nf)
+ | `Pacman -> `Pacman
+ and aux l =
+ function
+ #nf_nob as x -> (aux_nob l x :> nf)
+ | `Bottom -> `Bottom
in
(aux 0 t : nf)
;;
| `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
| `I((x,ar),args) ->
(if x < n then [] else [(x-n,ar)]) @
- List.concat (List.map (aux n) (Listx.to_list args))
+ List.concat (List.map (aux n) (Listx.to_list args :> nf list))
| `Lam(_,t) -> aux (n+1) t
| `Match(t,_,liftno,bs,args) ->
aux n (t :> nf) @
List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
- List.concat (List.map (aux n) args)
+ List.concat (List.map (aux n) (args :> nf list))
+ | `Bottom | `Pacman -> []
in aux 0
;;
let free_vars = (List.map fst) ++ free_vars';;
module ToScott =
struct
-let rec t_of_i_num_var =
+let rec scott_of_nf =
function
| `N n -> Scott.mk_n n
| `Var(v,_) -> Pure.V v
| `Match(t,_,liftno,bs,args) ->
- let bs = List.map (fun (n,t) -> n, t_of_nf (lift liftno t)) !bs in
- let t = t_of_i_num_var t in
+ let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in
+ let t = scott_of_nf (t :> nf) in
let m = Scott.mk_match t bs in
- List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
- | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
-and t_of_nf =
- function
- | #i_num_var as x -> t_of_i_num_var x
- | `Lam(b,f) -> Pure.L (t_of_nf f)
-
+ List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list)
+ | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx)
+ | `Lam(b,f) -> Pure.L (scott_of_nf f)
+ | `Bottom -> let f x = Pure.A (x,x) in f (Pure.L (f (Pure.V 0)))
+ | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
end
(************ Pretty-printing ************************************)
-let rec string_of_term l =
- let rec string_of_term_w_pars l = function
+(* let rec string_of_term l = fun _ -> "";; *)
+
+let rec string_of_term l =
+ let rec string_of_term_w_pars l = function
| `Var(n,ar) -> print_name l n ^ ":" ^ string_of_int ar
| `N n -> string_of_int n
- | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
+ | `I _ as t -> "(" ^ string_of_term_no_pars_app l t ^ ")"
| `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
| `Match(t,(v,ar),bs_lift,bs,args) ->
"[match("^ string_of_var v ^":"^ string_of_int ar ^") " ^ string_of_term_no_pars l (t :> nf) ^
- " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
- String.concat " " (List.map (string_of_term l) args) ^ ")"
- and string_of_term_no_pars_app l = function
- | `I((n,ar), args) -> print_name l n ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
+ " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift (t :> nf))) !bs) ^ "] " ^
+ String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
+ | `Bottom -> "TNT"
+ | `Pacman -> "PAC"
+ and string_of_term_no_pars_app l = function
+ | `I((n,ar), args) -> print_name l n ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args :> nf list))
| #nf as t -> string_of_term_w_pars l t
and string_of_term_no_pars_lam l = function
| `Lam(_,t) -> let name = string_of_var (List.length l) in
"λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
| _ as t -> string_of_term_no_pars l t
- and string_of_term_no_pars l : nf -> string = function
+ and string_of_term_no_pars l = function
| `Lam _ as t -> string_of_term_no_pars_lam l t
| #nf as t -> string_of_term_no_pars_app l t
in string_of_term_no_pars l
;;
let print ?(l=[]) = string_of_term l;;
-let string_of_nf t = string_of_term [] (t:>nf);;
+let string_of_nf t = string_of_term [] (t :> nf);;
(************ Hereditary substitutions ************************************)
let rec set_arity arity = function
| `Var(n,_) -> `Var(n,arity)
-| `N _ as t -> t
+| `N _ | `Bottom | `Pacman as t -> t
| `Lam(false, t) -> `Lam(false, set_arity arity t)
| `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
| `I _ | `Lam _ -> assert false
let minus1 n = if n = min_int then n else n - 1;;
let rec mk_app (h : nf) (arg : nf) =
-(*let res =*)
- match h with
- `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
- | `Var v -> `I(v, Listx.Nil arg)
- | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
- | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
- | `N _ -> assert false (* Numbers cannot be applied *)
+ match arg with
+ | `Bottom -> `Bottom
+ | #nf_nob as arg ->
+ match h with
+ | `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
+ | `Var v -> `I(v, Listx.Nil arg)
+ | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
+ | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
+ | `Bottom | `Pacman as t -> t
+ | `N _ -> assert false (* Numbers cannot be applied *)
(*in let l = ["v0";"v1";"v2"] in
prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
and mk_match t (n,ar) bs_lift bs args =
(*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
- match t with
+ let m =
+ match t with
`N m ->
(try
let h = List.assoc m !bs in
let h = set_arity (minus1 ar) h in
let h = lift bs_lift h in
- mk_appl h args
+ h
with Not_found ->
- `Match (t,(n,ar),bs_lift,bs,args))
- | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
+ `Match (t,(n,ar),bs_lift,bs,[]))
+ | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,[]) in
+ mk_appl m args
-and subst truelam delift_by_one what (with_what : nf) (where : nf) =
+and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) =
let rec aux_propagate_arity ar = function
| `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
| `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
function
`I((n,ar),args) ->
if n = what + l then
- mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
+ let args = Listx.map (aux l) (args :> nf Listx.listx) in
+ mk_appx (lift l (aux_propagate_arity ar (with_what :> nf))) args
else
- `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
+ mk_appl (`Var ((if delift_by_one && n >= l then n-1 else n), ar)) (List.map (aux l) (Listx.to_list (args :> nf Listx.listx)))
| `Var(n,ar) ->
if n = what + l then
- lift l (aux_propagate_arity ar with_what)
+ lift l (aux_propagate_arity ar (with_what :> nf))
else
`Var((if delift_by_one && n >= l then n-1 else n), ar)
| `N _ as x -> x
| `Match(t,v,bs_lift,bs,args) ->
let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
let l' = l - bs_lift in
- let with_what' = lift l' with_what in
+ let with_what' = lift l' (with_what :> nf) in
(* The following line should be the identity when delift_by_one = true because we
are assuming the ts to not contain lambda-bound variables. *)
bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
- mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) args)
+ mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) (args :> nf list))
and aux l(*lift*) =
(*function iii -> let res = match iii with*)
function
| #i_num_var as x -> aux_i_num_var l x
| `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
+ | `Bottom -> `Bottom
+ | `Pacman -> `Pacman
(*in let ll = ["v0";"v1";"v2"] in
prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
in
let rec aux t1 t2 = match t1, t2 with
| `Var(n,_) , `Var(m,_) -> compare n m
| `I((n1,_), l1), `I((n2,_), l2) ->
- clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
+ clex compare (lex aux) (n1, (Listx.to_list l1 :> nf list)) (n2, (Listx.to_list l2 :> nf list))
+ | `Bottom, `Bottom
+ | `Pacman, `Pacman -> 0
| `Lam _, `N _ -> -1
| `N _, `Lam _ -> 1
+ | `Bottom, `Lam _
+ | `Lam _, `Bottom -> assert false (* TO BE UNDERSTOOD *)
| `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
| `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
| t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
| `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
- clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
+ clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, (args :> nf list))) ((u' :> nf), (bs', (args' :> nf list)))
| `Match _, _ -> -1
| _, `Match _ -> 1
| `N _, _ -> -1
| _, `N _ -> 1
| `I _, _ -> -1
| _, `I _ -> 1
+ | `Bottom, _ -> -1
+ | _, `Bottom -> 1
+ | `Pacman, _ -> -1
+ | _, `Pacman -> 1
in aux x y
;;
if eta_eq sub t then true else
match t with
| `Lam(_,t') -> eta_subterm (lift 1 sub) t'
+ | `Bottom
+ | `Pacman -> false
| `Match(u,ar,liftno,bs,args) ->
eta_subterm sub (u :> nf)
|| List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
- || List.exists (eta_subterm sub) args
- | `I(v, args) -> List.exists (eta_subterm sub) (Listx.to_list args) || (match sub with
+ || List.exists (eta_subterm sub) (args :> nf list)
+ | `I(v, args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
| `Var v' -> v = v'
| `I(v', args') -> v = v'
&& Listx.length args' < Listx.length args
- && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
+ && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args :> nf list)) (Listx.to_list args' :> nf list))
| _ -> false
)
| `N _ | `Var _ -> false
let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
-
let max_arity_tms n =
let max a b = match a, b with
| None, None -> None
let aux_var l (m,a) = if n + l = m then Some a else None in
let rec aux l = function
| `Var v -> aux_var l v
- | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
+ | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms :> nf list))
| `Lam(_,t) -> aux (l+1) t
- | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
- | `N _ -> None
+ | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l (args :> nf list))) (aux_tms l (List.map snd !bs))
+ | `N _ | `Bottom | `Pacman -> None
and aux_tms l =
List.fold_left (fun acc t -> Pervasives.max acc (aux l t)) None in
fun tms -> aux_tms 0 (tms :> nf list)
;;
-
-let get_first_args var =
-let rec aux l = function
-| `Lam(_,t) -> aux (l+1) t
-| `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
-| `I((n,_), args) -> if n = var + l then [Listx.last args] else []
-| `N _
-| `Var _ -> []
-in aux 0
-;;
-
-let compute_arities m =
- let rec aux n tms =
- if n = 0
- then []
- else
- let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
- let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
- arity :: (aux (n-1) tms)
- in fun tms -> List.rev (aux m tms)
-;;
-
-let compute_arities var special_k all_tms =
- let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
- compute_arities special_k tms
-;;
-type var = int * int
-type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
-type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
-type 'nf i_num_var_ =
- [ `I of var * 'nf Listx.listx
- | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list
- | `N of int
- | `Var of var ]
-type 'nf nf_ =
- [ `I of var * 'nf Listx.listx
- | `Lam of bool * 'nf nf_
- | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list
- | `N of int
- | `Var of var ]
-type nf = nf nf_
-type i_var = nf i_var_
-type i_n_var = nf i_n_var_
-type i_num_var = nf i_num_var_
+type var = int * (* arity of variable*) int;;
+type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ]
+type 'nf_nob i_n_var_ = [ `N of int | 'nf_nob i_var_ ]
+type ('nf_nob,'nf) i_num_var_ = [
+ | 'nf_nob i_n_var_
+ | `Match of ('nf_nob,'nf) i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf_nob list
+]
+type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_,'nf) i_num_var_ ]
+type nf = [ nf nf_nob_ | `Bottom ]
+type nf_nob = nf nf_nob_
+type i_var = nf_nob i_var_;;
+type i_n_var = nf_nob i_n_var_;;
+type i_num_var = (nf_nob,nf) i_num_var_;;
val hd_of_i_var : i_var -> int
val hd_of : i_n_var -> int option
val arity_of_hd : i_n_var -> int
val free_vars : nf -> int list
module ToScott :
sig
- val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t
- val t_of_nf : nf -> Pure.Pure.t
+ val scott_of_nf : nf -> Pure.Pure.t
end
val print : ?l:string list -> nf -> string
val string_of_nf : [<nf] -> string
val mk_app : nf -> nf -> nf
val mk_appl : nf -> nf list -> nf
val mk_appx : nf -> nf Listx.listx -> nf
-val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf
+val mk_match : i_num_var -> var -> int -> (int * nf) list ref -> nf list -> nf
val subst : bool -> bool -> int -> nf -> nf -> nf
val parse' : string list -> nf list * string list
val eta_compare : nf -> nf -> int
val eta_eq : [< nf ] -> [< nf ] -> bool
val eta_subterm : [< nf ] -> [< nf ] -> bool
val max_arity_tms : int -> [< nf] list -> int option
-val compute_arities : int -> int -> nf list -> int list
val minus1 : int -> int
+++ /dev/null
-open Util
-open Util.Vars
-open Pure
-
-(************ Syntax ************************************)
-
-(* Normal forms*)
-
-(* Var n = n-th De Bruijn index, 0-based *)
-
-(*type nf =
- | Lam of nf
- | Var of int
- | i
-and i =
- | I of int * nf listx
-;;*)
-type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ]
-type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
-type 'nf i_num_var_ = [
- | 'nf i_n_var_
- | `Match of 'nf i_num_var_ * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
-]
-type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | `Bomb | `Pacman | 'nf i_num_var_ ]
-type nf = nf nf_
-type i_var = nf i_var_;;
-type i_n_var = nf i_n_var_;;
-type i_num_var = nf i_num_var_;;
-
-let hd_of_i_var =
- function
- `I (v,_)
- | `Var v -> v
-
-let hd_of =
- function
- `I (v,_)
- | `Var v -> Some v
- | `N _ -> None
- | `Match _ | `Bomb -> assert false
-
-let lift m (t : nf) =
- let rec aux_i_num_var l =
- function
- `I(n,args) -> (`I((if n < l then n else n+m),Listx.map (aux l) args) : i_num_var)
- | `Var n -> `Var (if n < l then n else n+m)
- | `N _ as x -> x
- | `Match(t,lift,bs,args) ->
- `Match(aux_i_num_var l t, lift + m, bs, List.map (aux l) args)
- and aux l =
- function
- #i_num_var as x -> (aux_i_num_var l x :> nf)
- | `Lam(b,nf) -> `Lam (b,aux (l+1) nf)
- | `Bomb -> `Bomb
- | `Pacman -> `Pacman
- in
- (aux 0 t : nf)
-;;
-
-(* put t under n lambdas, lifting t accordingtly *)
-let rec make_lams t =
- function
- 0 -> t
- | n when n > 0 -> `Lam (false,lift 1 (make_lams t (n-1)))
- | _ -> assert false
-
-let free_vars =
- let rec aux n = function
- `N _ -> []
- | `Var x -> if x < n then [] else [x-n]
- | `I(x,args) ->
- (if x < n then [] else [x-n]) @
- List.concat (List.map (aux n) (Listx.to_list args))
- | `Lam(_,t) -> aux (n+1) t
- | `Match(t,liftno,bs,args) ->
- aux n (t :> nf) @
- List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
- List.concat (List.map (aux n) args)
- | `Bomb | `Pacman -> []
- in aux 0
-;;
-
-module ToScott =
-struct
-
-let rec t_of_i_num_var =
- function
- | `N n -> Scott.mk_n n
- | `Var v -> Pure.V v
- | `Match(t,liftno,bs,args) ->
- let bs = List.map (fun (n,t) -> n, t_of_nf (lift liftno t)) !bs in
- let t = t_of_i_num_var t in
- let m = Scott.mk_match t bs in
- List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
- | `I(v, args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
-and t_of_nf =
- function
- | #i_num_var as x -> t_of_i_num_var x
- | `Lam(b,f) -> Pure.L (t_of_nf f)
- | `Bomb -> let f x = Pure.A (x,x) in f (Pure.L (f (Pure.V 0)))
- | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
-
-end
-
-
-(************ Pretty-printing ************************************)
-
-(* let rec print ?(l=[]) =
- function
- `Var n -> print_name l n
- | `N n -> string_of_int n
- | `Match(t,bs_lift,bs,args) ->
- "([" ^ print ~l (t :> nf) ^
- " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^
- String.concat " " (List.map (print ~l) args) ^ ")"
- | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
- | `Lam(_,nf) ->
- let name = string_of_var (List.length l) in
- "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf)
-;; *)
-
-let rec string_of_term l =
- let rec string_of_term_w_pars l = function
- | `Var n -> print_name l n
- | `N n -> string_of_int n
- | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
- | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
- | `Match(t,bs_lift,bs,args) ->
- "(match " ^ string_of_term_no_pars l (t :> nf) ^
- " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
- String.concat " " (List.map (string_of_term l) args) ^ ")"
- | `Bomb -> "TNT"
- | `Pacman -> "PAC"
- and string_of_term_no_pars_app l = function
- | `I(n, args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
- | #nf as t -> string_of_term_w_pars l t
- and string_of_term_no_pars_lam l = function
- | `Lam(_,t) -> let name = string_of_var (List.length l) in
- "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
- | _ as t -> string_of_term_no_pars l t
- and string_of_term_no_pars l : nf -> string = function
- | `Lam _ as t -> string_of_term_no_pars_lam l t
- | #nf as t -> string_of_term_no_pars_app l t
- in string_of_term_no_pars l
-;;
-
-let rec print ?(l=[]) = string_of_term l;;
-
-(************ Hereditary substitutions ************************************)
-
-let cast_to_i_var =
- function
- #i_var as y -> (y : i_var)
- | t ->
- prerr_endline (print (t :> nf));
- assert false (* algorithm failed *)
-
-let cast_to_i_n_var =
- function
- #i_n_var as y -> (y : i_n_var)
- | t ->
- prerr_endline (print (t :> nf));
- assert false (* algorithm failed *)
-
-let cast_to_i_num_var =
- function
- #i_num_var as y -> (y : i_num_var)
- | t ->
- prerr_endline (print (t :> nf));
- assert false (* algorithm failed *)
-
-let rec mk_app (h : nf) (arg : nf) =
-(*let res =*)
- match h with
- `I(n,args) -> `I(n,Listx.append (Listx.Nil arg) args)
- | `Var n -> `I(n, Listx.Nil arg)
- | `Lam(_,nf) -> subst true 0 arg (nf : nf)
- | `Match(t,lift,bs,args) -> `Match(t,lift,bs,List.append args [arg])
- | `N _ -> assert false (* Numbers cannot be applied *)
- | `Bomb | `Pacman -> failwith "mk_app su bomba o pacman"
-(*in let l = ["v0";"v1";"v2"] in
-prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
-
-and mk_appl h args =
- (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
- List.fold_left mk_app h args
-
-and mk_appx h args = Listx.fold_left mk_app h args
-
-and mk_match t bs_lift bs args =
- (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
- match t with
- `N m ->
- (try
- let h = List.assoc m !bs in
- let h = lift bs_lift h in
- mk_appl h args
- with Not_found ->
- `Match (t,bs_lift,bs,args))
- | `I _ | `Var _ | `Match _ -> `Match(t,bs_lift,bs,args)
-
-and subst delift_by_one what (with_what : nf) (where : nf) =
- let rec aux_i_num_var l =
- function
- `I(n,args) ->
- if n = what + l then
- mk_appx (lift l with_what) (Listx.map (aux l) args)
- else
- `I ((if delift_by_one && n >= l then n-1 else n), Listx.map (aux l) args)
- | `Var n ->
- if n = what + l then
- lift l with_what
- else
- `Var (if delift_by_one && n >= l then n-1 else n)
- | `N _ as x -> x
- | `Match(t,bs_lift,bs,args) ->
- let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
- let l' = l - bs_lift in
- let with_what' = lift l' with_what in
- (* The following line should be the identity when delift_by_one = true because we
- are assuming the ts to not contain lambda-bound variables. *)
- bs := List.map (fun (n,t) -> n,subst false what with_what' t) !bs ;
- mk_match (cast_to_i_num_var (aux_i_num_var l t)) bs_lift bs (List.map (aux l) args)
- and aux l(*lift*) =
-(*function iii -> let res = match iii with*)
- function
- | #i_num_var as x -> aux_i_num_var l x
- | `Lam(b,nf) -> `Lam(b,aux (l+1) nf)
- | `Bomb -> `Bomb
- | `Pacman -> `Pacman
-(*in let ll = ["v0";"v1";"v2"] in
-prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
- in
- aux 0 where
-;;
-
-(************ Parsing ************************************)
-
-let parse' strs =
- let rec aux = function
- | Parser.Lam t -> `Lam (true,aux t)
- | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2)
- | Parser.Var v -> `Var v
- in let (tms, free) = Parser.parse_many strs
- in (List.map aux tms, free)
-;;
-
-(************** Algorithm(s) ************************)
-
-let eta_eq x y =
- let rec aux = function
- | `Var n , `Var m -> n = m
- | `I(n1, l1), `I(n2, l2) ->
- n1 = n2 && Listx.length l1 = Listx.length l2 &&
- List.for_all aux (List.combine (Listx.to_list l1) (Listx.to_list l2))
- | `Lam(_,t1), `Lam(_,t2) -> aux (t1,t2)
- | `Lam(_,t1), t2
- | t2, `Lam(_,t1) -> aux( t1, (mk_app (lift 1 t2) (`Var 0)) )
- | `N n1, `N n2 -> n1 = n2
- | `Match(u,bs_lift,bs,args), `Match(u',bs_lift',bs',args') ->
- aux ((u :> nf), (u' :> nf)) && List.length !bs = List.length !bs' &&
- let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
- let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
- List.for_all (fun ((n,t),(n',t')) -> n = n' && aux (t, t')) (List.combine bs bs') && List.length args = List.length args' &&
- List.for_all aux (List.combine args args')
- | _ -> false
- in aux (x, y)
-;;
-
-let eta_compare x y =
- if eta_eq x y then 0 else compare x y
-;;
-
-let eta_eq (#nf as x) (#nf as y) = eta_eq x y;;
-
-let rec eta_subterm sub t =
- if eta_eq sub t then true else
- match t with
- | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
- | `Match(u,liftno,bs,args) ->
- eta_subterm sub (u :> nf)
- || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
- || List.exists (eta_subterm sub) args
- | `I(v, args) -> List.exists (eta_subterm sub) (Listx.to_list args) || (match sub with
- | `Var v' -> v = v'
- | `I(v', args') -> v = v'
- && Listx.length args' < Listx.length args
- && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
- | _ -> false
- )
- | `N _ | `Var _ | `Bomb | `Pacman -> false
-;;
-
-let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
+++ /dev/null
-type 'nf i_var_ = [ `I of int * 'nf Listx.listx | `Var of int ]
-type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
-type 'nf i_num_var_ =
- [ `I of int * 'nf Listx.listx
- | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list
- | `N of int
- | `Var of int ]
-type 'nf nf_ =
- [ `I of int * 'nf Listx.listx
- | `Lam of bool * 'nf nf_
- | `Match of 'nf i_num_var_ * int * (int * 'nf) list ref * 'nf list
- | `N of int
- | `Var of int
- | `Bomb
- | `Pacman ]
-type nf = nf nf_
-type i_var = nf i_var_
-type i_n_var = nf i_n_var_
-type i_num_var = nf i_num_var_
-val hd_of_i_var : i_var -> int
-val hd_of :
- [< `I of 'a * 'b | `Match of 'c | `N of 'd | `Var of 'a ] -> 'a option
-(* put t under n lambdas, lifting t accordingtly *)
-val make_lams : nf -> int -> nf
-val lift : int -> nf -> nf
-val free_vars : nf -> int list
-module ToScott :
- sig
- val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t
- val t_of_nf : nf -> Pure.Pure.t
- end
-val print : ?l:string list -> nf -> string
-val cast_to_i_var : [< nf > `I `Var] -> i_var
-val cast_to_i_n_var : [< nf > `I `N `Var] -> i_n_var
-val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var
-val mk_app : nf -> nf -> nf
-val mk_appl : nf -> nf list -> nf
-val mk_appx : nf -> nf Listx.listx -> nf
-val mk_match : nf i_num_var_ -> int -> (int * nf) list ref -> nf list -> nf
-val subst : bool -> int -> nf -> nf -> nf
-val parse' : string list -> nf list * string list
-val eta_compare : nf -> nf -> int
-val eta_eq : [< nf ] -> [< nf ] -> bool
-val eta_subterm : [< nf ] -> [< nf ] -> bool
projects / fireball-separation.git / commitdiff